package tr.edu.ege.kipler.satisfiability.completion.rules.dl;

import java.util.Iterator;
import java.util.Set;

import tr.edu.ege.kipler.satisfiability.BranchingException;
import tr.edu.ege.kipler.satisfiability.ReasonerException;
import tr.edu.ege.kipler.satisfiability.Reasoner;
import tr.edu.ege.kipler.satisfiability.completion.rules.nondeterminism.NominalGuessBranchingPoint;
import tr.edu.ege.kipler.satisfiability.container.ConceptCategory;
import tr.edu.ege.kipler.satisfiability.container.Individual;
import tr.edu.ege.kipler.satisfiability.container.SHOIQABox;
import tr.edu.ege.kipler.satisfiability.container.operational.DisjointIndividualDetector;
import tr.edu.ege.kipler.satisfiability.container.operational.FilterType;
import tr.edu.ege.kipler.satisfiability.container.operational.RelatedIndividualWithTypeFilterFactory;
import tr.edu.ege.kipler.syntax.Role;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.concept.Concept;
import tr.edu.ege.kipler.syntax.concept.QualifiedNoRestriction;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class NominalGuessRule extends ABoxRule {
	private SHOIQABox aBox;

	private boolean applied;

	private Reasoner prover;

	public NominalGuessRule(Reasoner prover) {
		this.prover = prover;
	}

	@Override
	public void apply() throws ReasonerException {
		applied = false;
		aBox = (SHOIQABox) getWorld().getABox();
		Individual x = getIndividual();
		if (aBox.isNominal(x)) {
			for (Iterator<Concept> i = x
					.conceptIterator(ConceptCategory.AT_MOST); i.hasNext();) {
				QualifiedNoRestriction qr = (QualifiedNoRestriction) i.next();
				if (hasBlockableSPredecessor(x, qr)
						&& !hasMDifferentNominalNeighbors(x, qr)) {
					NominalGuessBranchingPoint bp = new NominalGuessBranchingPoint();
					bp.setWcs(getWcs());
					bp.setWorld(getWorld());
					bp.setIndividual(getIndividual());
					ConceptAssertion branchCause = new ConceptAssertion(qr,
							getIndividual().getName());
					bp.setBranchCause(branchCause);
					prover.addBranch(bp);
					getWcs().getData().getLogger().info(
							"WCS " + getWcs().getId()
									+ " Nominal guess rule: Branching for "
									+ branchCause);
					applied = true;
					throw new BranchingException();
				}
			}
		}
	}

	@Override
	public boolean isApplied() {
		return applied;
	}

	private boolean hasMDifferentNominalNeighbors(Individual x,
			QualifiedNoRestriction origQr) {
		boolean result = false;
		for (Iterator<Concept> i = x.conceptIterator(ConceptCategory.AT_MOST); i
				.hasNext()
				&& !result;) {
			QualifiedNoRestriction qr = (QualifiedNoRestriction) i.next();
			if (qr.getNo() >= 1 && qr.getNo() <= origQr.getNo()
					&& qr.getRole().equals(origQr.getRole())
					&& qr.getConcept().equals(origQr.getConcept())) {
				Set<Individual> neighbors = getNominalSNeighborsWithTypeC(qr
						.getRole(), x, qr.getConcept());
				if (neighbors.size() >= qr.getNo()) {
					DisjointIndividualDetector detector = new DisjointIndividualDetector(
							aBox, neighbors);
					if (detector.hasSetWithMinCardinality(qr.getNo())) {
						result = true;
						break;
					}
				}
			}
		}
		return result;
	}

	private Set<Individual> getNominalSNeighborsWithTypeC(Role role,
			Individual owner, Concept concept) {
		return RelatedIndividualWithTypeFilterFactory.getFilter(
				FilterType.TYPED_NOMINAL_NEIGHBOR, aBox, owner, role, concept)
				.filter();
	}

	private boolean hasBlockableSPredecessor(Individual x,
			QualifiedNoRestriction qr) {
		return RelatedIndividualWithTypeFilterFactory.getFilter(
				FilterType.TYPED_BLOCKABLE_PREDECESSOR, aBox, x, qr.getRole(),
				qr.getConcept()).contains();
	}

}
